<html>
<head><meta charset="utf-8"><title>unification under binders · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html">unification under binders</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="180629295"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629295" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629295">(Nov 13 2019 at 14:13)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> so, I was looking at your <a href="https://github.com/rust-lang/chalk/pull/282" target="_blank" title="https://github.com/rust-lang/chalk/pull/282">zip_binders PR</a></p>



<a name="180629378"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629378" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629378">(Nov 13 2019 at 14:14)</a>:</h4>
<p>and the issue it fixes, which links to the <a href="https://github.com/rust-lang/chalk/blob/3ea7a60b73e202f2799efa8d711b633ed55b276a/src/test/unify.rs#L122-L145" target="_blank" title="https://github.com/rust-lang/chalk/blob/3ea7a60b73e202f2799efa8d711b633ed55b276a/src/test/unify.rs#L122-L145">equality_binder test</a></p>



<a name="180629392"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629392" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629392">(Nov 13 2019 at 14:14)</a>:</h4>
<p>yep</p>



<a name="180629398"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629398" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629398">(Nov 13 2019 at 14:14)</a>:</h4>
<p>I have a question about that test</p>



<a name="180629424"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629424" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629424">(Nov 13 2019 at 14:14)</a>:</h4>
<p>(I'm reminded there was one comment that was niggling at me in that PR that I meant go back and adjust, but carry on)</p>



<a name="180629449"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629449" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629449">(Nov 13 2019 at 14:14)</a>:</h4>
<p>yes, I think that comment was confusing me as well :)</p>



<a name="180629452"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629452" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629452">(Nov 13 2019 at 14:14)</a>:</h4>
<p>but also</p>



<a name="180629469"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629469" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629469">(Nov 13 2019 at 14:15)</a>:</h4>
<p>actually I believe it was referencing a different test</p>



<a name="180629473"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629473" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629473">(Nov 13 2019 at 14:15)</a>:</h4>
<p>the issue, that is</p>



<a name="180629489"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629489" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629489">(Nov 13 2019 at 14:15)</a>:</h4>
<p>I think that <code>equality_binder</code> test was behaving correctly before?</p>



<a name="180629523"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629523" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629523">(Nov 13 2019 at 14:15)</a>:</h4>
<p>though I think I can also anticipate what your question is about it</p>



<a name="180629543"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629543" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629543">(Nov 13 2019 at 14:15)</a>:</h4>
<p>I see that it generates a constraint for <code>?0</code> (which is <code>'a</code> in the <code>exists&lt;'a&gt;</code>) to equal <code>'!2_0</code> (which I think corresponds to <code>'c</code> in <code>for&lt;'c&gt;</code>)</p>



<a name="180629606"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629606" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629606">(Nov 13 2019 at 14:16)</a>:</h4>
<p>can such a constraint ever be satisfied?</p>



<a name="180629615"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629615" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629615">(Nov 13 2019 at 14:16)</a>:</h4>
<p>Yes and no</p>



<a name="180629621"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629621" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629621">(Nov 13 2019 at 14:16)</a>:</h4>
<p>In this example, no</p>



<a name="180629649"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629649" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629649">(Nov 13 2019 at 14:16)</a>:</h4>
<p>However</p>



<a name="180629662"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629662" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629662">(Nov 13 2019 at 14:17)</a>:</h4>
<p>you could imagine an example like this</p>



<a name="180629691"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629691" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629691">(Nov 13 2019 at 14:17)</a>:</h4>
<p>(..but in the <code>equality_binder2</code> test it can?)</p>



<a name="180629730"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629730" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629730">(Nov 13 2019 at 14:17)</a>:</h4>
<div class="codehilite"><pre><span></span>forall&lt;&#39;a&gt; {
    forall&lt;T&gt; {
        forall&lt;&#39;b&gt; {
            if (&#39;a: &#39;b, &#39;b: &#39;a) {
                T = &amp;&#39;b u32
            }
        }
    }
}
</pre></div>



<a name="180629794"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629794" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629794">(Nov 13 2019 at 14:18)</a>:</h4>
<p>Sorry, like that</p>



<a name="180629826"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629826" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629826">(Nov 13 2019 at 14:18)</a>:</h4>
<p>In this case, 'b cannot be named by T</p>



<a name="180629833"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629833" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629833">(Nov 13 2019 at 14:18)</a>:</h4>
<p>but 'a <em>can</em></p>



<a name="180629840"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629840" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629840">(Nov 13 2019 at 14:18)</a>:</h4>
<p>and 'b is equivalent to 'a</p>



<a name="180629845"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629845" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629845">(Nov 13 2019 at 14:18)</a>:</h4>
<p>chalk can't really reason about that</p>



<a name="180629860"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629860" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629860">(Nov 13 2019 at 14:18)</a>:</h4>
<p>this is actually a topic I would like to use as an upcoming design meeting</p>



<a name="180629870"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629870" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629870">(Nov 13 2019 at 14:18)</a>:</h4>
<p>right, okay</p>



<a name="180629897"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629897" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629897">(Nov 13 2019 at 14:19)</a>:</h4>
<p>as I've not fully tried to write out all my thoughts about it</p>



<a name="180629933"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629933" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629933">(Nov 13 2019 at 14:19)</a>:</h4>
<p>but I do not think it is chalk's job to solve these sorts of things, in short</p>



<a name="180629937"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629937" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629937">(Nov 13 2019 at 14:19)</a>:</h4>
<p>or .. well, it's a mix</p>



<a name="180629956"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629956" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629956">(Nov 13 2019 at 14:19)</a>:</h4>
<p>I want chalk to do some of this work, and export some of it to polonius :)</p>



<a name="180629988"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180629988" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180629988">(Nov 13 2019 at 14:20)</a>:</h4>
<p>anyway, the setup as is is not I think quite perfect, but basically what it tries to do right <em>now</em> is to always generate a constraint, and not assume much of anything</p>



<a name="180630041"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630041" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630041">(Nov 13 2019 at 14:20)</a>:</h4>
<p>yeah, I'm a little confused by that.. clearly in the logic we have stuff that requires "reasoning about lifetimes," e.g. your example :)</p>



<a name="180630073"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630073" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630073">(Nov 13 2019 at 14:20)</a>:</h4>
<p>well</p>



<a name="180630083"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630083" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630083">(Nov 13 2019 at 14:20)</a>:</h4>
<p>I would draw the line there</p>



<a name="180630109"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630109" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630109">(Nov 13 2019 at 14:20)</a>:</h4>
<p>the trait solver does not, for the most part, reason about lifetimes</p>



<a name="180630122"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630122" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630122">(Nov 13 2019 at 14:20)</a>:</h4>
<p>nor does the type-checker</p>



<a name="180630140"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630140" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630140">(Nov 13 2019 at 14:20)</a>:</h4>
<p>but I think it <em>should</em> be able to reason a <em>bit</em> about them, specifically in connection with universes</p>



<a name="180630174"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630174" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630174">(Nov 13 2019 at 14:21)</a>:</h4>
<blockquote>
<p>the trait solver does not, for the most part, reason about lifetimes</p>
</blockquote>
<p>this statment is maybe too strong</p>



<a name="180630183"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630183" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630183">(Nov 13 2019 at 14:21)</a>:</h4>
<p>what I mean is, it doesn't really know which lifetimes outlive which other ones</p>



<a name="180630195"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630195" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630195">(Nov 13 2019 at 14:21)</a>:</h4>
<p>that is more of an <em>output</em> from trait solving</p>



<a name="180630199"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630199" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630199">(Nov 13 2019 at 14:21)</a>:</h4>
<p>which lifetimes <em>must</em> outlive which other ones</p>



<a name="180630206"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630206" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630206">(Nov 13 2019 at 14:21)</a>:</h4>
<p>that is fed into polonius to see if it is satisfiable</p>



<a name="180630266"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630266" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630266">(Nov 13 2019 at 14:22)</a>:</h4>
<p>okay, right</p>



<a name="180630271"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630271" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630271">(Nov 13 2019 at 14:22)</a>:</h4>
<p>(but Polonius shouldn't have the job of figuring out the hgiher-ranked relationships, that's something we can figure out)</p>



<a name="180630291"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630291" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630291">(Nov 13 2019 at 14:22)</a>:</h4>
<p>this is related to some pending rustc PRs too</p>



<a name="180630296"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630296" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630296">(Nov 13 2019 at 14:22)</a>:</h4>
<p>I guess one thing I'm missing is, what does chalk <em>do</em> with the <code>'a: 'b, 'b: 'a</code> condition above?</p>



<a name="180630308"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630308" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630308">(Nov 13 2019 at 14:22)</a>:</h4>
<p>right now, nothing</p>



<a name="180630319"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630319" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630319">(Nov 13 2019 at 14:23)</a>:</h4>
<p>in fact, we can't even express that right now I don't think</p>



<a name="180630343"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630343" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630343">(Nov 13 2019 at 14:23)</a>:</h4>
<p>but I think eventually it would use that</p>



<a name="180630360"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630360" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630360">(Nov 13 2019 at 14:23)</a>:</h4>
<p>specifically when it sees a <code>'a: 'b</code> that is must prove, it would use logic like this:</p>



<a name="180630377"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630377" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630377">(Nov 13 2019 at 14:23)</a>:</h4>
<ul>
<li>if both regions are in root universe, generate the consrtaint as an output (more on this in a sec) for polonius to solve</li>
</ul>



<a name="180630481"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630481" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630481">(Nov 13 2019 at 14:24)</a>:</h4>
<ul>
<li>but if one of them  (say 'b, as in this case) is a placeholder, search the environment for things like <code>'x: 'b</code></li>
</ul>



<a name="180630499"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630499" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630499">(Nov 13 2019 at 14:24)</a>:</h4>
<p>in which case, we can try to prove <code>'a: 'x</code></p>



<a name="180630634"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630634" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630634">(Nov 13 2019 at 14:24)</a>:</h4>
<p>the goal would be eventually to find root regions we can convert to outputs</p>



<a name="180630648"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630648" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630648">(Nov 13 2019 at 14:24)</a>:</h4>
<p>I've mocked this up in lambda prolog</p>



<a name="180630661"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630661" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630661">(Nov 13 2019 at 14:24)</a>:</h4>
<p>I've been meaning to mock it up in chalk...</p>



<a name="180630687"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630687" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630687">(Nov 13 2019 at 14:25)</a>:</h4>
<p>there would also be a base rule that <code>forall&lt;'x&gt; { 'static: 'x }</code></p>



<a name="180630709"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630709" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630709">(Nov 13 2019 at 14:25)</a>:</h4>
<p>anway if you apply it to this example, the output would be some constraints like <code>'a: 'a</code>, which is clearly true</p>



<a name="180630718"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630718" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630718">(Nov 13 2019 at 14:25)</a>:</h4>
<p>(And we could just filter them out)</p>



<a name="180630739"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630739" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630739">(Nov 13 2019 at 14:25)</a>:</h4>
<p>does that make sense?</p>



<a name="180630753"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630753" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630753">(Nov 13 2019 at 14:25)</a>:</h4>
<p>hmm I think so</p>



<a name="180630845"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630845" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630845">(Nov 13 2019 at 14:26)</a>:</h4>
<p>you are motivating me to try and write this up</p>



<a name="180630854"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630854" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630854">(Nov 13 2019 at 14:26)</a>:</h4>
<p>so it seems like, very naively, you could end up with complex constraints which introduced their own binders</p>



<a name="180630878"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630878" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630878">(Nov 13 2019 at 14:26)</a>:</h4>
<p>yes can have complex constraints, but they will not have their own binders</p>



<a name="180630884"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630884" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630884">(Nov 13 2019 at 14:26)</a>:</h4>
<p>our current constraints do</p>



<a name="180630891"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630891" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630891">(Nov 13 2019 at 14:26)</a>:</h4>
<p>but this is a shift from that approach</p>



<a name="180630895"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630895" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630895">(Nov 13 2019 at 14:26)</a>:</h4>
<p>and are basically a "subset of chalk goals involving only lifetimes"</p>



<a name="180630915"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630915" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630915">(Nov 13 2019 at 14:27)</a>:</h4>
<p>the idea is that chalk can handle the binders, in short, but it <em>can't</em> figure out the root constraints</p>



<a name="180630921"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630921" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630921">(Nov 13 2019 at 14:27)</a>:</h4>
<p>okay, I see</p>



<a name="180630929"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630929" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630929">(Nov 13 2019 at 14:27)</a>:</h4>
<p>one downside is</p>



<a name="180630940"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630940" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630940">(Nov 13 2019 at 14:27)</a>:</h4>
<p>that we wll get cosnrtaints like <code>'a: 'b || 'a: 'c</code></p>



<a name="180630942"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630942" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630942">(Nov 13 2019 at 14:27)</a>:</h4>
<p>that's nonobvious to me, but interesting</p>



<a name="180630950"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630950" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630950">(Nov 13 2019 at 14:27)</a>:</h4>
<p>i.e., one of these must be true, but not both</p>



<a name="180630952"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630952" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630952">(Nov 13 2019 at 14:27)</a>:</h4>
<p>but that is already true</p>



<a name="180630960"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630960" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630960">(Nov 13 2019 at 14:27)</a>:</h4>
<p>we have to deal with it somehow, i'm not sure the best way to handle it</p>



<a name="180630969"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630969" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630969">(Nov 13 2019 at 14:27)</a>:</h4>
<p>right, I remember us talking about that</p>



<a name="180630970"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180630970" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180630970">(Nov 13 2019 at 14:27)</a>:</h4>
<p>today's rustc sometimes just gives ambiguous results</p>



<a name="180631022"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180631022" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180631022">(Nov 13 2019 at 14:28)</a>:</h4>
<p>I would like to get to the point where we have that problem</p>



<a name="180631024"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180631024" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180631024">(Nov 13 2019 at 14:28)</a>:</h4>
<p>and then worry about it :)</p>



<a name="180631036"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180631036" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180631036">(Nov 13 2019 at 14:28)</a>:</h4>
<p>for now I think we can be conservative, rustc presently is</p>



<a name="180631042"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180631042" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180631042">(Nov 13 2019 at 14:28)</a>:</h4>
<p>at least I think so :)</p>



<a name="180631053"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180631053" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180631053">(Nov 13 2019 at 14:28)</a>:</h4>
<p>:)</p>



<a name="180631067"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180631067" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180631067">(Nov 13 2019 at 14:28)</a>:</h4>
<p>in short I want to isolate that problem to the "interface" betwen chalk and polonius</p>



<a name="180631073"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180631073" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180631073">(Nov 13 2019 at 14:28)</a>:</h4>
<p>chalk can generate the precise constraint</p>



<a name="180631087"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180631087" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180631087">(Nov 13 2019 at 14:28)</a>:</h4>
<p>maybe we simplify it, or make it more conservative, and then hand it off to polonius</p>



<a name="180631101"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180631101" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180631101">(Nov 13 2019 at 14:28)</a>:</h4>
<p>or maybe we even run polonius many times (one for each <code>||</code>)</p>



<a name="180631102"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180631102" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180631102">(Nov 13 2019 at 14:29)</a>:</h4>
<p>until we find a sol'n</p>



<a name="180631112"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/unification%20under%20binders/near/180631112" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/unification.20under.20binders.html#180631112">(Nov 13 2019 at 14:29)</a>:</h4>
<p>that's the worst case</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>